1. Field of the Invention
The present invention is directed to system for determining the extent that a design has been or can be verified.
2. Description of the Related Art
As circuit designs become more complex, the cost of manufacturing increases and the time-to-market becomes even more critical, it has become apparent that circuit designers must verify their designs prior to manufacturing. That is, after a given circuit is designed, the circuit designer will perform tests or simulations using a computer to verify that the circuit design will operate as intended. For example, a circuit designer may use a schematic capture program to draw a circuit or may use a hardware description language to describe a circuit. The circuit designer will then create tests in order to simulate operation of the circuit.
Even if a design passes the tests created by the designer, it does not mean that the circuit will operate as intended. There may be various modes of behavior which are not verified by the designer""s tests. Therefore, there is a need to know whether the tests provided by the designer are exhaustive. That is, the designer needs to know if some portion of the design has not been tested.
One previous attempt to verify designs and determine the amount of verification has included writing test vectors. Test vectors are sets of inputs to a circuit which are used by a simulator to simulate the operation of the circuit. A designer must write the test vector manually or use software to create the test vectors. It typically takes a long time to write a sufficient set of test vectors and rarely do these test vectors provide one hundred percent coverage. Another drawback of using test vectors is that the time needed to run the simulation using the test vectors can be extremely long, even to the point where the design process becomes unreasonably stalled. If the simulation using test vectors reveals that additional vectors are needed, the designer must then create additional test vectors which takes even more time and run the entire simulation again. Because time to market is critical and engineering resources are expensive, the prior solution for providing verification of a design is not sufficient.
The present invention, roughly described, includes a system for providing static coverage analysis. The system receives at least two inputs including a hardware description and a set of properties. The system determines what portions of the design can and cannot be verified using the set of properties. In one embodiment, the invention includes three levels of analysis. Each level provides a different tradeoff between accuracy and speed.
One embodiment of the present invention is based on signal coverage. A signal is uncovered if a change in the gate driving the signal does not change the outcome of verification. An input variable, which by definition is not the output of any gate, is considered uncovered if tying it down to a constant value (e.g. zero or one) does not change the outcome of verification.
One embodiment of the present invention provides for incremental analysis. That is, subsequent iterations of the process can be refined to only look at the new properties and/or those portions of the design that were not previously covered by the existing properties. The present invention provides a static analysis, which means that test vectors are not used to simulate over time. Because the invention uses a static analysis, run time is significantly shorter than using test vectors.
In one embodiment, the present invention includes a method for determining verification coverage of a set of properties. The method includes the steps of reading a set of properties, reading a design and determining what portions of the design can be verified by the set of properties without using test vectors. In one embodiment, the step of determining includes the steps of choosing a property, choosing one or more appropriate variables in the property, determining fan-in for the chosen one or more appropriate variables and marking the signals in the determined fan-in as being covered. In another embodiment, the step of determining includes the steps of propagating constants for a given property, removing constants from the property, choosing one or more appropriate variables in the property, determining fan-in for one or more chosen appropriate variables and marking the signals in the determined fan-in as being covered. In yet another embodiment, the step of determining may also include the steps of propagating constants for a property, making signals as being partially covered, removing constants from the property, determining a cone of logic for the property, choosing a signal and an uncovered fault, verifying the design using the set of properties and the first signal at the uncovered fault, reporting the first signal if no properties failed, and repeating the process for other signals and uncovered faults.
The present invention can be implemented using software, hardware, or a combination of software and hardware. When all or portions of the present invention are implemented in software, that software can reside on a processor readable storage medium. Examples of an appropriate processor readable storage medium include a floppy disk, hard disk, CD-ROM, memory IC, etc. The hardware used to implement the present invention includes an output device (e.g. a monitor or printer), an input device (e.g. a keyboard, pointing device, etc.), a processor in communication with the output device and processor readable storage medium in communication with the processor. The processor readable storage medium stores code capable of programming the processor to perform the steps to implement the present invention. In one embodiment, the processor reads the properties and the design from the processor readable storage medium. The process of the present invention can also be implemented on a web page on the Internet or on a server that can be accessed over communication lines.